perm filename EXOTIC.XGP[W82,JMC] blob
sn#638810 filedate 1982-01-26 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ α∧␈↓␈↓ u1
␈↓ α∧␈↓α␈↓ ∧bEXOTIC CONTINUOUS FUNCTIONALS
␈↓ α∧␈↓α1. Some examples of exotic continuous functionals.
␈↓ α∧␈↓␈↓ αTThe␈αfixed␈αpoint␈αtheory␈αof␈αrecursive␈αfunctions␈αis␈αbased␈αon␈αcontinuous␈αfunctionals␈αsuch␈αas␈α␈↓ t␈↓
␈↓ α∧␈↓defined by
␈↓ α∧␈↓1)␈↓ αt ␈↓↓␈↓ t␈↓↓[f](x) = ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ g x ␈↓αelse␈↓↓ m(x,f h x)␈↓.
␈↓ α∧␈↓␈↓ αTThe␈α∞theory␈α∞tells␈α∞us␈α∞that␈α∞each␈α∞continuous␈α∞monotonic␈α∞functional␈α∞has␈α∞a␈α∞fixed␈α∞point,␈α∞and␈α
we
␈↓ α∧␈↓study␈α⊃the␈α⊃fixed␈α⊃points␈α∩of␈α⊃those␈α⊃functionals␈α⊃involved␈α⊃in␈α∩recursive␈α⊃definitions.␈α⊃ In␈α⊃the␈α∩case␈α⊃of
␈↓ α∧␈↓recursive␈α
definitions␈α␈↓↓␈↓ t␈↓↓[f](x)␈↓␈α
is␈α
a␈αform␈α
in␈αwhich␈α
␈↓↓f␈↓␈α
appears␈αas␈α
a␈αfunction␈α
symbol.␈α
However,␈αthese
␈↓ α∧␈↓are␈α⊂not␈α⊂all␈α⊂the␈α⊂continuous␈α⊂functions␈α⊂there␈α⊂are,␈α∂and␈α⊂it␈α⊂may␈α⊂be␈α⊂interesting␈α⊂to␈α⊂study␈α⊂some␈α∂other
␈↓ α∧␈↓examples. Consider functionals of the form
␈↓ α∧␈↓2)␈↓ αt ␈↓↓␈↓ t␈↓↓[f](x) = ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ g x ␈↓αelse␈↓↓ m f␈↓∧ -1␈↓↓ h x␈↓;
␈↓ α∧␈↓that's␈αright,␈αwe␈αmean␈αthe␈αinverse␈αof␈αthe␈αfunction␈α␈↓↓f␈↓.␈α In␈αorder␈αto␈αmake␈αthe␈αfunctional␈αwell␈αdefined
␈↓ α∧␈↓and␈α
continuous,␈αwe␈α
make␈α
the␈αfollowing␈α
stipulations:␈αFirst,␈α
the␈α
variable␈α␈↓↓x␈↓␈α
ranges␈αover␈α
non-negative
␈↓ α∧␈↓integers and ␈↓↓f␈↓ is a partial function from integers to integers. Second, we define ␈↓↓f␈↓∧ -1␈↓↓␈↓ by
␈↓ α∧␈↓3)␈↓ αt ␈↓↓f␈↓∧ -1␈↓↓(y) = ␈↓ m␈↓↓ x.(f(x) = y)␈↓,
␈↓ α∧␈↓where
␈↓ α∧␈↓4)␈↓ αt ␈↓↓␈↓ m␈↓↓ x.p(x) ← least(0,p)␈↓,
␈↓ α∧␈↓and ␈↓↓least(y,p)␈↓ is recursively defined by
␈↓ α∧␈↓5)␈↓ αt ␈↓↓least(y,p) ← ␈↓αif␈↓↓ p(y) ␈↓αthen␈↓↓ y ␈↓αelse␈↓↓ least(y+1,p)␈↓.
␈↓ α∧␈↓Note␈α∩that␈α∩the␈α∩recursive␈α∩definition␈α⊃insures␈α∩that␈α∩␈↓↓f␈↓∧␈α∩-1␈↓↓␈↓␈α∩is␈α⊃continuous␈α∩in␈α∩␈↓↓f,␈↓␈α∩and␈α∩that␈α∩␈↓ m␈↓x.␈↓↓p(x)␈↓␈α⊃is
␈↓ α∧␈↓undefined␈α
if␈α
there␈α
is␈α
a␈α
value␈α
of␈α
␈↓↓x␈↓␈α
for␈α
which␈α
␈↓↓p(x)␈↓␈α
is␈α
undefined␈α
lower␈α
than␈α
a␈α
value␈α
for␈α
which␈α
␈↓↓p(x)␈↓␈α
is
␈↓ α∧␈↓true.␈α Without␈αthis␈αproperty,␈α␈↓↓least(x,p)␈↓␈αwouldn't␈αbe␈αmonotonic␈αin␈α␈↓↓p␈↓,␈αand␈αthere␈αmightn't␈αbe␈αa␈αleast
␈↓ α∧␈↓fixed point.
␈↓ α∧␈↓␈↓ αTConsider specializing (2) to
␈↓ α∧␈↓6)␈↓ αt ␈↓↓␈↓ t␈↓↓1[f](x) = ␈↓αif␈↓↓ x = 0 ␈↓αthen␈↓↓ 0 ␈↓αelse␈↓↓ 2 + f␈↓∧ -1␈↓↓(x - 1)␈↓.
␈↓ α∧␈↓The fixed point ␈↓↓f1␈↓ of ␈↓ t␈↓1 may be computed by iterating ␈↓ t␈↓1 on ␈↓ W␈↓, getting
␈↓ α∧␈↓7)␈↓ αt ␈↓↓f1 x = ␈↓αif␈↓↓ x = 0 ␈↓αthen␈↓↓ 0 ␈↓αelse␈↓↓ ␈↓αif␈↓↓ x = 1 ␈↓αthen␈↓↓ 2 ␈↓αelse␈↓↓ ␈↓αif␈↓↓ x = 3 ␈↓αthen␈↓↓ 3 ␈↓αelse␈↓↓ ␈↓ w␈↓↓␈↓,
␈↓ α∧␈↓which seems exotic if not pathological.
␈↓ α∧␈↓␈↓ αTWolf␈α⊂Polak␈α⊂points␈α⊂out␈α⊃that␈α⊂while␈α⊂␈↓ t␈↓1␈α⊂is␈α⊂exotic,␈α⊃its␈α⊂fixed␈α⊂point␈α⊂is␈α⊂an␈α⊃ordinary␈α⊂recursive
␈↓ α∧␈↓function, since the recursive computation of ␈↓↓f␈↓∧ -1␈↓↓␈↓ can be spelled out. Thus
␈↓ α∧␈↓␈↓ εddraft␈↓ u2
␈↓ α∧␈↓8)␈↓ αt ␈↓↓f1 x ← ␈↓αif␈↓↓ x = 0 ␈↓αthen␈↓↓ 0 ␈↓αelse␈↓↓ 2 + f2(0,x-1)␈↓,
␈↓ α∧␈↓where
␈↓ α∧␈↓9)␈↓ αt ␈↓↓f2(y,x) ← ␈↓αif␈↓↓ f1(x) = y ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ f2(y+1,x)␈↓.
␈↓ α∧␈↓␈↓ αTHere is another weird functional:
␈↓ α∧␈↓10)␈↓ αt ␈↓↓␈↓ t␈↓↓2[f](x) = ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ g x ␈↓αelse␈↓↓ ␈↓αif␈↓↓ f h1 x = ␈↓ w␈↓↓ ∧ f h2 x = ␈↓ w␈↓↓ ␈↓αthen␈↓↓ ␈↓ w␈↓↓ ␈↓αelse␈↓↓ f h3 x␈↓,
␈↓ α∧␈↓where␈α␈↓↓p,␈↓␈α␈↓↓g,␈↓␈α␈↓↓h1,␈↓␈α␈↓↓h2␈↓␈αand␈α␈↓↓h3␈↓␈αare␈αall␈αassumed␈αtotal.␈α (Equality␈αhere␈αis␈αtaken␈αin␈αthe␈αstrong␈αsense␈αin
␈↓ α∧␈↓which␈α
its␈α
value␈αis␈α
always␈α
␈↓αtrue␈↓␈α
or␈α␈↓αfalse␈↓␈α
and␈α
is␈α
never␈αundefined).␈α
Computing␈α
␈↓↓␈↓ t␈↓↓2[f](x)␈↓␈α
involves␈αa
␈↓ α∧␈↓parallel␈αcomputation␈αof␈α␈↓↓f␈αh1␈α
x␈↓␈αand␈α␈↓↓f␈αh2␈αx␈↓;␈α
if␈αeither␈αsucceeds,␈αthe␈αother␈α
can␈αbe␈αstopped.␈α It␈αis␈α
easily
␈↓ α∧␈↓seen␈α
that␈αthe␈α
functional␈α
is␈αcontinuous␈α
and␈α
hence␈αhas␈α
a␈α
fixed␈αpoint␈α
-␈α
call␈αit␈α
␈↓↓f2.␈↓␈α
If␈αwe␈α
can␈αuse␈α
LISP
␈↓ α∧␈↓functions, we can write an ordinary recursive definition of ␈↓↓f2,␈↓ namely
␈↓ α∧␈↓11)␈↓ αt ␈↓↓f2 x ← ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ g x ␈↓αelse␈↓↓ (λy. f2 h3 x)(f2'(list(x),qNIL))␈↓,
␈↓ α∧␈↓with
␈↓ α∧␈↓12)␈↓ αt␈α␈↓↓f2'(u,v)␈α←␈α␈↓αif␈↓↓␈α␈↓αn␈↓↓␈αu␈α␈↓αthen␈↓↓␈α(␈↓αn␈↓↓␈αv␈α∨␈αf2(v,␈↓NIL␈↓↓))␈α␈↓αelse␈↓↓␈αp␈αh1␈α␈↓αa␈↓↓␈αu␈α∨␈αp␈αh2␈α␈↓αa␈↓↓␈αu␈α∨␈αf2'(␈↓αd␈↓↓␈αu,␈αh1␈α␈↓αa␈↓↓␈αu␈α.
␈↓ α∧␈↓↓(h2 ␈↓αa␈↓↓ u . v))␈↓.
␈↓ α∧␈↓[Carolyn␈α
Talcott␈αpoints␈α
out␈α
that␈αthe␈α
above␈α
redefinition␈αis␈α
not␈α
correct␈αand␈α
has␈α
an␈αalternate␈α
breadth
␈↓ α∧␈↓first search, but hadn't proved hers correct to her satisfaction at last discussion].
␈↓ α∧␈↓If␈αwe␈α
are␈αnot␈α
allowed␈αto␈α
use␈αLISP␈αfunctions,␈α
then␈α␈↓↓f2␈↓␈α
may␈αbe␈α
one␈αof␈α
Hewitt's␈αand␈αPaterson's␈α
(197x)
␈↓ α∧␈↓examples of functions that can be written with parallel programs but not with recursive programs.
␈↓ α∧␈↓α2. When is a functional definable by a term?
␈↓ α∧␈↓␈↓ αTIn␈α
view␈α
of␈α
the␈α
above␈α
examples,␈α
we␈α
can␈α
try␈α
to␈α
characterize␈α
those␈α
continuous␈α
functional␈α
for
␈↓ α∧␈↓which␈α␈↓↓␈↓ t␈↓↓[f](x)␈↓␈αcan␈αbe␈αwritten␈αas␈αa␈αterm␈αin␈α␈↓↓f␈↓␈αand␈α␈↓↓x␈↓␈αin␈αwhich␈α␈↓↓f␈↓␈αappears␈αas␈αa␈αfunction␈αsymbol␈αand␈α␈↓↓x␈↓
␈↓ α∧␈↓as an individual variable. Let's call them ␈↓↓term functionals␈↓.
␈↓ α∧␈↓␈↓ αTIf␈α
␈↓ t␈↓␈αis␈α
a␈αcontinuous␈α
functional,␈α
then␈αthe␈α
value␈αof␈α
␈↓↓␈↓ t␈↓↓[f](x)␈↓␈α
depends␈αon␈α
the␈αvalue␈α
of␈α
␈↓↓f(y)␈↓␈αfor
␈↓ α∧␈↓only␈αa␈αfinite␈αnumber␈αof␈α
␈↓↓y␈↓'s.␈α Namely,␈αthere␈αexist␈α␈↓↓y␈↓β1␈↓↓, ... ,y␈↓βk␈↓␈αsuch␈α
that␈α␈↓↓f(y)␈↓␈αcan␈αbe␈αchanged␈αfor␈α
any
␈↓ α∧␈↓␈↓↓y␈↓␈α⊂different␈α∂from␈α⊂the␈α⊂␈↓↓y␈↓βi␈↓'s␈α∂without␈α⊂changing␈α⊂the␈α∂value␈α⊂of␈α∂␈↓↓␈↓ t␈↓↓[f](x)␈↓.␈α⊂ In␈α⊂general␈α∂␈↓↓k␈↓␈α⊂depends␈α⊂on␈α∂the
␈↓ α∧␈↓particular␈α␈↓↓f␈↓␈αand␈α␈↓↓x,␈↓␈αbut␈αwhen␈α␈↓ t␈↓␈αis␈αa␈αterm␈αfunctional,␈α␈↓↓k␈↓␈αis␈αbounded␈αby␈αthe␈αnumber␈αof␈αoccurrences
␈↓ α∧␈↓of␈α␈↓↓f␈↓␈αin␈αthe␈α
term␈α␈↓↓␈↓ t␈↓↓[f](x)␈↓.␈α In␈αour␈αfirst␈α
exotic␈αexample,␈αthe␈αnumber␈α
of␈α␈↓↓f(y)␈↓␈αon␈αwhich␈α␈↓↓␈↓ t␈↓↓[f](x)␈↓␈α
depends
␈↓ α∧␈↓is␈αunbounded,␈αbecause,␈αdepending␈αon␈α␈↓↓f,␈↓␈αany␈αfinite␈αnumber␈αof␈αof␈α␈↓↓f(x)␈↓'s␈αmay␈αhave␈αto␈αbe␈αexamined
␈↓ α∧␈↓to␈α∞compute␈α∞␈↓↓f␈↓∧␈α
-1␈↓↓(y)␈↓.␈α∞ Tentatively,␈α∞we␈α∞shall␈α
call␈α∞a␈α∞functional␈α∞where␈α
such␈α∞a␈α∞bound␈α∞exists␈α
␈↓↓uniformly
␈↓ α∧␈↓↓continuous␈↓,␈α
although␈α
we␈α∞have␈α
not␈α
yet␈α
been␈α∞able␈α
to␈α
establish␈α
any␈α∞properties␈α
in␈α
common␈α∞with␈α
the
␈↓ α∧␈↓corresponding property in analysis. Thus all ␈↓↓term functionals␈↓ are ␈↓↓uniformly continuous␈↓.
␈↓ α∧␈↓␈↓ αTThe␈α∩second␈α∪exotic␈α∩functional␈α∪is␈α∩uniformly␈α∩continuous␈α∪but␈α∩still␈α∪isn't␈α∩a␈α∪term␈α∩functional.
␈↓ α∧␈↓Indeed every term functional has the another property that we may call ␈↓↓sequentiality␈↓:
␈↓ α∧␈↓␈↓ εddraft␈↓ u3
␈↓ α∧␈↓␈↓ αTSuppose␈α∃that␈α∃in␈α∃evaluating␈α∀␈↓↓␈↓ t␈↓↓[f](x)␈↓,␈α∃we␈α∃have␈α∃already␈α∃evaluated␈α∀␈↓↓f(x1),f(x2), ...,f(xk)␈↓.
␈↓ α∧␈↓There␈α
are␈α
two␈α
possibilities;␈α∞Either␈α
the␈α
value␈α
of␈α
␈↓↓␈↓ t␈↓↓[f](x)␈↓␈α∞is␈α
already␈α
determined␈α
by␈α
these␈α∞values␈α
or
␈↓ α∧␈↓␈↓↓f(y)␈↓␈αmust␈αbe␈αcomputed␈αfor␈αadditional␈α␈↓↓y␈↓'s.␈α We␈αcall␈α␈↓ t␈↓␈α␈↓↓sequential␈↓␈αif␈αin␈αthe␈αlatter␈αcase␈αthere␈αis␈αalways
␈↓ α∧␈↓at␈αleast␈α
one␈α␈↓↓y␈↓␈α
such␈αthat␈α
␈↓↓␈↓ t␈↓↓[f](x)␈↓ = ␈↓ w␈↓␈αunless␈α␈↓↓f(y) ≠ ␈↓ w␈↓↓␈↓.␈α
The␈αfunction␈α
␈↓ t␈↓2␈αof␈α
the␈αprevious␈α
section␈αis
␈↓ α∧␈↓not sequential. If ␈↓ t␈↓ is sequential we can always write
␈↓ α∧␈↓13)␈↓ αt␈α∪␈↓↓␈↓ t␈↓↓[f](x)␈α∩=␈α∪␈↓αif␈↓↓␈α∪p1␈α∩x␈α∪␈↓αthen␈↓↓␈α∪g1␈α∩x␈α∪␈↓αelse␈↓↓␈α∪{f␈α∩h1␈α∪x}[λx1.␈↓αif␈↓↓␈α∪p2(x,x1)␈α∩␈↓αthen␈↓↓␈α∪g2(x,x1)␈α∪␈↓αelse␈↓↓␈α∩{f
␈↓ α∧␈↓↓h2(x,x1)}[λx2.␈↓αif␈↓↓ p3(x,x1,x2) ␈↓αthen␈↓↓ g3(x,x1,x2) ␈↓αelse␈↓↓ {f h3(x,x1,x2}[λx3.␈↓αif␈↓↓ ... etc. ]]]␈↓.
␈↓ α∧␈↓[We␈αuse␈αthe␈αnotation␈α␈↓↓{arg}fn␈↓␈αfor␈α␈↓↓fn(arg)␈↓␈αwhen␈αit␈αis␈αmore␈αconvenient␈αto␈αwrite␈αthe␈αargument␈αbefore
␈↓ α∧␈↓the function].
␈↓ α∧␈↓[Note␈αof␈αFeb␈α9,␈α1979:␈αThe␈αabove␈αis␈αnot␈αquite␈αright,␈αbecause␈α␈↓ t␈↓␈αmay␈αevaluate␈α␈↓↓f␈↓␈αapplied␈αto␈αvarious
␈↓ α∧␈↓constants before asking for any of the actual arguments ␈↓↓x,␈↓ ␈↓↓y,␈↓ etc.].
␈↓ α∧␈↓␈↓ αTWe can avoid the lengthening formulas of (13) by writing
␈↓ α∧␈↓14)␈↓ αt␈α∂␈↓↓␈↓ t␈↓↓[f](x0)␈α⊂=␈α∂␈↓αif␈↓↓␈α⊂p1␈α∂x0␈α⊂␈↓αthen␈↓↓␈α∂g1␈α⊂x0␈α∂␈↓αelse␈↓↓␈α∂{m1(x0,f␈α⊂h1␈α∂x0)}[λx1.␈↓αif␈↓↓␈α⊂p2␈α∂x1␈α⊂␈↓αthen␈↓↓␈α∂g2␈α⊂x1␈α∂␈↓αelse␈↓↓
␈↓ α∧␈↓↓{m2(x1,f h2 x1)}[λx2.␈↓αif␈↓↓ p3 x2 ␈↓αthen␈↓↓ ␈↓etc.
␈↓ α∧␈↓␈↓ αTGiven␈αthat␈α␈↓ t␈↓␈αis␈αsequential,␈αthere␈αare␈αtwo␈αpossibilities.␈α If␈α␈↓ t␈↓␈αis␈αalso␈α␈↓↓uniformly␈αcontinuous␈↓␈αthe
␈↓ α∧␈↓sequence␈α⊂of␈α⊂terms␈α⊂given␈α⊂in␈α⊂(13)␈α⊂will␈α⊂be␈α⊂finite␈α∂-␈α⊂otherwise␈α⊂not.␈α⊂ If␈α⊂the␈α⊂␈↓↓p␈↓'s,␈α⊂␈↓↓g␈↓'s␈α⊂and␈α⊂␈↓↓h␈↓'s␈α⊂are␈α∂all
␈↓ α∧␈↓computable␈α∩in␈α∪some␈α∩collection␈α∪␈↓↓C␈↓␈α∩of␈α∪base␈α∩functions,␈α∩then␈α∪we␈α∩will␈α∪call␈α∩␈↓ t␈↓␈α∪computable␈α∩if␈α∪it␈α∩is
␈↓ α∧␈↓sequential and bounded. In that case its least fixed point will also be a computable function in ␈↓↓C␈↓.
␈↓ α∧␈↓␈↓ αTWhile␈α∂sequentiality␈α∂requires␈α∂that␈α∂some␈α∂␈↓↓f(x)␈↓␈α∂be␈α∂required␈α∂for␈α∂the␈α∂definedness␈α∂of␈α∂␈↓↓␈↓ t␈↓↓[f](x)␈↓,␈α∞it
␈↓ α∧␈↓doesn't require that ␈↓↓h(x)␈↓ be unique. Thus if
␈↓ α∧␈↓15)␈↓ αt ␈↓↓␈↓ t␈↓↓[f](x) = f(m x) + f(n x)␈↓,
␈↓ α∧␈↓we can take either ␈↓↓h1 x = m x␈↓ or ␈↓↓h1 x = n x␈↓.
␈↓ α∧␈↓α3. Additional remarks.
␈↓ α∧␈↓␈↓ αT1. Here are some more continuous ␈↓↓␈↓ t␈↓↓[f](x)␈↓:
␈↓ α∧␈↓a. ␈↓↓f(x) ≠ ␈↓ w␈↓↓␈↓ for at least one ␈↓↓x.␈↓
␈↓ α∧␈↓b. ␈↓↓f(x)+x ε A␈↓ for at least 20 odd values of ␈↓↓x.␈↓
␈↓ α∧␈↓c. ␈↓↓R1(x,f h1 x) ∧ R2(x,f f h2 x)␈↓ for at least 20 ␈↓↓x.␈↓
␈↓ α∧␈↓d. The functional
␈↓ α∧␈↓␈↓ αT␈↓↓␈↓ t␈↓↓[f](x) = ␈↓αif␈↓↓ p1 x ␈↓αthen␈↓↓ g x ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ∃z.(f h1 z ≠ ␈↓ w␈↓↓) ␈↓αthen␈↓↓ f h2 z ␈↓αelse␈↓↓ ␈↓ w␈↓↓␈↓
␈↓ α∧␈↓is␈αcontinuous.␈α It␈αcan't␈αbe␈αcomputed␈αfor␈αgeneral␈α␈↓↓f␈↓␈αexcept␈αby␈αparallel␈αevaluator,␈αbut␈αits␈αfixed␈αpoint
␈↓ α∧␈↓can apparently be sequentially computed provided the domain of ␈↓↓x␈↓ can be effectively enumerated.
␈↓ α∧␈↓␈↓ εddraft␈↓ u4
␈↓ α∧␈↓␈↓ αT2.␈α
Note␈αthat␈α
␈↓↓a␈↓␈α
thru␈α␈↓↓c␈↓␈α
above␈αare␈α
predicates,␈α
and␈αthe␈α
essential␈αpart␈α
of␈α
␈↓↓d␈↓␈αis␈α
also␈α
a␈αpredicate.
␈↓ α∧␈↓Predicates␈αplay␈αa␈α
special␈αrole,␈αbecause␈α
it␈αis␈αeasier␈α
to␈αdefine␈αexotic␈α
continuous␈αpredicates␈αthan␈α
other
␈↓ α∧␈↓functions. The space whose elements are just T and ␈↓ w␈↓ seems to play a special role.
␈↓ α∧␈↓␈↓ αT3.␈α⊂This␈α⊂paper␈α⊂is␈α⊂related␈α⊂to␈α⊃the␈α⊂problem␈α⊂of␈α⊂intensional␈α⊂properties␈α⊂of␈α⊃recursive␈α⊂programs
␈↓ α∧␈↓through␈α
the␈αidea␈α
that␈α
intensional␈αproperties␈α
of␈αone␈α
program␈α
are␈αextensional␈α
properties␈αof␈α
"derived
␈↓ α∧␈↓programs".␈α It␈αis␈αimportant␈αto␈αask␈αwhich␈αproperties␈αof␈αa␈αprogram␈αare␈αextensional␈αproperties␈αof␈α
the
␈↓ α∧␈↓functional.␈α⊃ It␈α⊃appears␈α⊃that␈α⊃the␈α⊃property␈α∩of␈α⊃being␈α⊃iterative␈α⊃is␈α⊃an␈α⊃extensional␈α⊃property␈α∩of␈α⊃the
␈↓ α∧␈↓functional.
␈↓ α∧␈↓Also␈αmaximum␈αrequired␈αdepth␈αof␈αrecursion.␈α The␈αtest␈αas␈αto␈αwhether␈αa␈αa␈αfinite␈αapproximation␈αa-
␈↓ α∧␈↓list␈α
is␈α
ok␈α
is␈α
f-extensional.␈α
A␈α
function␈α
generating␈α
a␈α
finite␈α
approximation␈α
that␈α
evaluates␈α
␈↓↓x␈↓␈α∞is␈α
not.
␈↓ α∧␈↓What␈αis␈αthe␈α
next␈αlevel␈αup␈αfrom␈α
the␈αfunctional?␈α f(x)+f(x)␈αand␈α
2f(x)␈αgive␈αthe␈αsame␈α
functional␈αbut
␈↓ α∧␈↓different␈α
computation␈αsequence␈α
cbn␈αor␈α
cbv.␈α If␈α
we␈α
change␈αa␈α
recursive␈αprogram␈α
by␈αputting␈α
in␈αa␈α
test
␈↓ α∧␈↓that␈α
is␈αnever␈α
true,␈α
then␈αwe␈α
don't␈α
change␈αthe␈α
computation␈α
sequence.␈α The␈α
number␈α
of␈αoccurrences␈α
of
␈↓ α∧␈↓the atom CAR in the program is changed.
␈↓ α∧␈↓Perhaps␈α⊂can␈α⊂be␈α⊂put␈α⊂into␈α⊂"sequential␈α⊂form"␈α⊂or␈α⊂changed␈α⊂to␈α⊂"sequential␈α⊂form",␈α⊂and␈α⊂then␈α⊂certain
␈↓ α∧␈↓properties will become sequential.
␈↓ α∧␈↓John McCarthy
␈↓ α∧␈↓Artificial Intelligence Laboratory
␈↓ α∧␈↓Computer Science Department
␈↓ α∧␈↓Stanford University
␈↓ α∧␈↓Stanford, California 94305
␈↓ α∧␈↓ARPANET: MCCARTHY@SU-AI
␈↓ α∧␈↓␈↓εThis draft of EXOTIC[W77,JMC] PUBbed at 1:24 on January 26, 1982.␈↓